feat(CombinatoryLogic): Partrec → SKI computability#403
feat(CombinatoryLogic): Partrec → SKI computability#403jessealama wants to merge 13 commits intoleanprover:mainfrom
Conversation
There was a problem hiding this comment.
Looks pretty good to me! The title should probably say that only one direction of the equivalence is proven here (Partrec -> SKI). If I have time I can do a more thorough review but my only real concern would be whether the new version of primitive recursion could use the original one in Recursion.lean any more (though I would believe that the pair/unpair dance makes that impossible)
jessealama
force-pushed
the
ski-equivalence
branch
from
50924e4 to
c31c74d
Compare
jessealama
changed the title
In an earlier version of this proof, I tried to apply the original recursor directly but gave up because it was getting too bulky. The new |
Makes sense! happy for you to leave as-is and/or hide the definition as you & the maintainers prefer. I suppose the ideal outcome would be for the definition of the term to mirror what the function looks like in |
|
Converting to draft — splitting out the Sqrt/NatPair/NatUnpair layer as a smaller PR first: #445. |
|
@jessealama Can you resolve the merge conflicts here please? |
Prove that every Nat.Partrec function on ℕ is SKI-computable (nat_partrec_ski_computable). Translates all eight Nat.Partrec.Code constructors to SKI terms and proves correctness, exercising the Recursion.lean infrastructure: primitive recursion (Rec), μ-recursion (RFind/RFindAbove), Nat pairing/unpairing, and integer square root.
…ntions Shorten verbose docstrings, collapse rw/have/subst patterns to obtain rfl, extract inline calc blocks, and rename to camelCase (natPartrec_skiComputable, rfindAbove_induction).
Only one direction (Partrec → SKI) is proven; rename file and section header to avoid overclaiming equivalence. Remove unrelated SKIPartrec stub (converse direction) to a separate branch.
Add computes_of_total and RFindAbove_unfold helpers to eliminate repeated proof patterns. Simplify comp/pair_computes Part.mem chains and rfindAbove_induction via early subst + local helper. Remove dormant @[scoped grind] attributes from nil_correct and neg_correct.
jessealama
force-pushed
the
ski-equivalence
branch
from
23e7a99 to
6d3692c
Compare
Split the conjunction into `rfind_eval_root` (f evaluates to 0 at the root) and `rfind_eval_pos_below` (f evaluates to nonzero below k).
Done! I'd like to leave this as a draft for now; I'm a bit unhappy with a couple of the proofs and will spend some time cleaning them up. I'm open to any suggestions, of course, but just as a matter of review priority, I'm happy to put this on your backburner. |
Add RFindAbove_correct' which works with pointwise Church encoding properties rather than requiring a total function. Restate the original RFindAbove_correct as a corollary.
- Extract prec_computes and rfind_computes as standalone lemmas, making codeToSKINat_correct a uniform 1-2 line per case induction. - Delete rfindAbove_induction (40 lines) by using the generalized RFindAbove_correct' from Recursion.lean. - Add bind_eq_some helper to simplify Part.mem_bind_iff extraction boilerplate in comp_computes and prec_rec_correct.
|
@thomaskwaring I've done a bit of refactoring here that touches on Recursion.lean. I added a |
Promote the private helper to Part.eq_some_of_bind_eq_some in a new shared foundations file, making it available to other modules.
CI checkInitImports requires all Cslib modules to import Cslib.Init.
3 participants
Prove that every Nat.Partrec function on ℕ is SKI-computable (nat_partrec_ski_computable). Translates all eight Nat.Partrec.Code constructors to SKI terms and proves correctness, exercising the Recursion.lean infrastructure: primitive recursion (Rec), μ-recursion (RFind/RFindAbove), Nat pairing/unpairing, and integer square root.
Depends on leanprover-community/mathlib4#37521